es:ES, ff:FIFO, f2f+:F2F+-decls, sndr, rcvr:ff.C, e, e':E.
f2f+-pred(e,e')  [e: rcvr is_ack  sndr]  [e': sndr is_req   rcvr] 

latex

Definitions	P  Q, P & Q, x:A. B(x), ES, t  T, FIFO, F2F+-decls, ff.C, E, f2f+-pred(e',e), is_ack , [e: i p j], is_req
Lemmas	snd-it wf, f2f+Ack wf, f2f+-pred wf, es-E wf, fifoC wf, F2F+-decls wf, FIFO wf, event system wf, f2f+-pred-alternates